$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop). EquivRel $1$,$2$:$T$ List. $1$ agree\_on($T$;$a$.$P$($a$)) $2$